Process Calculi
Overview * Calculus of Communicating Systems * Calculus of Higher Order Broadcasting Systems * Calculus of Higher Order Communicating Systems * Communicating Sequential Processes Algebraic Theory of Processes The page Algebraic Theory of Processes is a study of the book by Matthew Hennsessy. Thoughts on A Sequential Broadcast Calculus There is a progression from CHOCS → CHOBS → ???, as a working name call this CHOAS. p ::= \epsilon \;\; \Big| \;\; x \;\; \Big| \;\; p ??x \;\; \Big| \;\; p !! p \;\; \Big| \;\; p . p \;\; \Big| \;\; p \; \times \; p \;\; \Big| \;\; p \; \pm\!\!\downarrow p \;\; \Big| \;\; p \; \pm\!\!\uparrow p Some ideas, a very basic process: ??x.x ??x.x \; \times \; !! ( ??x.x ) ACHOO - A Calculus of Higher Order Objects : s ::= 0 \;\; \Big| \;\; 1 \;\; \Big| \;\; j \;\; \Big| \;\; s !! s \;\; \Big| \;\; s ?? s \;\; \Big| \;\; s + s \;\; \Big| \;\; s . s \;\; \Big| \;\; s \setminus s \;\; \Big| \;\; s \; / \; s Calculus of Higher Order Processes We consider the following language: : p ::= 0 \;\; \Big| \;\; 1 \;\; \Big| \;\; j \;\; \Big| \;\; p !! p \;\; \Big| \;\; p ?? p \;\; \Big| \;\; p + p \;\; \Big| \;\; p . p \;\; \Big| \;\; p \setminus p \;\; \Big| \;\; p \; / \; p 0, 1, j are called atoms. A process evolves by emitting a process: : P_1 \xrightarrow{\quad P_2 \quad} P_3 P_2 will always be of the form: : P_2 = P_{2c} !! P_{2m} P_{2c} is called the channel process. P_{2m} is called the message process. P_2 is called a broadcast. A process can only evolve if it has a future and an active present. "." is called time composition. : P = P_p . P_f P_p is called the past of P = P_p . P_f . P_f is called the future of P = P_p . P_f . The basis of broadcasts can be summarised as follows: : 1!!1.P_f \xrightarrow{\quad 1!!1 \quad} P_f Composition example 1: : (1!!1 + 1!!1).P_f \xrightarrow{\quad 1!!(1 + 1) \quad} P_f Composition example 2: : (1!!1.P_1) + (1!!1..P_2) \xrightarrow{\quad 1!!(1 + 1) \quad} P_1 + P_2 Composition example 3: : (1!!1 + j!!1).P_f \xrightarrow{\quad (1!!1) + (j!!1) \quad} P_f Meanings How are the following interpreted? : (P_1 + P_2).P_3 Examlpes of this are: : (C_1!!M_1 + C_2!!M_2).P This case is straight forward, both messages are broadcast. : (C_1??M_1 + C_2??M_2).P This is more complex as there could be some ambiguity, for example: : (C_1??1 + C_2??1).P This could be a way of introducing non-determinism. A more difficult example is: : (C_1!!M_1 + C_2!!M_2.P_2).P For broadcasts this is not too difficult to solve, since broadcasts are essentially autonomus. The situation is more diffult for receives. : (C_1??M_1 + C_2??M_2.P_2).P One possible approach is that C_1??M_1 binds P but P does not become active until (C_1??M_1 + C_2??M_2.P_2) completes, if and when it does. Examples Example 1. : (1 + j)!!(j + 1).0 \xrightarrow{\quad (1 + j)!!(j + 1) \quad} 0 Example 2. : (((1 + j)!!(j + 1)) + ((1 + j)??1)).1 \xrightarrow{\quad (1 + j)!!(j + 1) \quad} (j + 1) Example 3. : (((1 + j)!!(j + 1)) + ((j + 1)??1)).1 \xrightarrow{\quad (1 + j)!!(j + 1) \quad} 0 Example 4. This is the same as example 2 but more readable. : \begin{array}{l} \begin{array}{rcl} \text{Let } \alpha & = & 1 + j \\ \text{Let } v & = & j + 1 \\ \text{Let } x & = & 1 \\ \\ \end{array} \\ ((\alpha !! v) + (\alpha ?? x)).x \xrightarrow{\quad \alpha !! v \quad} v \end{array} Example 5. : ((1 !! j) \backslash (1 !! j)).P \xrightarrow{\quad (1 !! j) \backslash (1 !! j) \quad} P Example 6. : (((1 !! j) \backslash (1 !! j)) + (1 ?? j)).P \xrightarrow{\quad (1 !! j) \backslash (1 !! j) \quad} P References * A Calculus of Broadcasting Systems, (Prasad, 1995) * Calculus of Broadcasting Systems - wikipedia. * Communicating Sequential Processes, (Hoare, 1985) * Towards a Primitive Higher Order Calculus of Broadcasting Systems, (Ostrovsky et al., 2002) Category:Research Category:Education